1. Field
The embodiments discussed herein are directed to a verification method, a verification apparatus, and a program, and more particularly to a verification method, a verification apparatus, and a program, which are suitable for verifying an asynchronous circuit.
2. Description of the Related Art
Operations of semiconductor integrated circuits are required to be verified through simulation with higher accuracy in a shorter time due to more-advanced functions and higher packing densities of the semiconductor integrated circuits. In particular, it has become more important recently to perform verification of an asynchronous circuit, which verifies a malfunction generated at an asynchronous point where circuit sections operating with different clock signals are connected to each other.
FIG. 1 is a flowchart illustrating a flow of circuit design and verification in the related art.
FIG. 1 also illustrates databases 80, 81, 82 and 83 for storing various kinds of data produced during circuit design and verification in the related art.
In circuit design for an LSI (Large Scale Integrated Circuit), the logical function of the circuit is first described at a register transfer level (RTL) by using a hardware description language (HDL) (operation S80). Then, logical verification is performed through RTL simulation to confirm the logical functional operation of the circuit (operation S81). If the logical functional operation is not what was expected, the flow returns to operation S80 in which the logical function of the circuit is described again at the RTL.
If the logical functional operation is what was expected, logical synthesis is executed to produce a netlist at a gate level (operation S82).
Then, formal verification (logical equivalence verification) of the circuit description between the netlist and the RTL is executed to confirm that the logic in the produced netlist is equivalent to the logic at the RTL (operation S83). If the logic in the produced netlist is not equivalent to the logic at the RTL, the flow returns to operation S80. In operation S80, the logical function of the circuit is described again at the RTL.
If the logical equivalence is confirmed, layout is executed to produce a netlist and delay information in SDF (Standard Delay Format) of actual wiring that is subjected to timing adjustment, addition of a test circuit, etc. (operation S84).
Then, the logical functional operation of the circuit and timing specs are confirmed based on the netlist and the delay information of the actual wiring. The logical functional operation of the circuit and timing specs are confirmed by performing timing verification by using a static timing analyzer (STA), as well logical verification and timing verification through dynamic simulation at a gate level (operation S85). If the timing specs are not satisfied, the flow returns to operation S80. In operation S80, the logical function of the circuit is described again at the RTL.
After the logical verification and the timing verification, a prototype chip is manufactured (operation S86), and confirmation of the operation is made based on evaluation of the actual chip (operation S87). If the operation of the actual chip is not what was expected, or if there is a problem in the circuit logic, the flow returns to operation S80 in which the logical function of the circuit is described again at the RTL. If there is a problem in the timing, though not shown, the flow returns to operation S84 in which layout is executed again.
If the evaluation of the actual chip is satisfied, mass production of the chips is started (operation S88). The LSI circuit design is thus completed.
In the above-described known process of circuit design and verification, the verification of the asynchronous circuit is usually executed in the RTL stage (operation S81) (see, e.g., Japanese Laid-open patent publication No. 2005-284426, No. 2004-185311, No. 2003-233638, and No. 2001-229211).
However, the known verification of the asynchronous circuit has a problem as follows. Even when the RTL verification proves that the circuit is operated without troubles, a malfunction is generated at an asynchronous point in some cases in the stage of the netlist produced after the logical synthesis.
FIGS. 2A and 2B illustrate respectively an RTL description and an asynchronous circuit represented by the netlist produced after the logical synthesis.
The portion of the RTL described in FIG. 2A shows that a value of B is substituted in C if A is 1, in sync with the rise of a clock signal CK1. Two paths may be generated between A_reg and C_reg, as illustrated in FIG. 2B, in an asynchronous circuit that is produced by the logical synthesis and includes two kinds of clock signals CK1 (100 MHz) and CK2 (200 MHz), even if only one path exists from A to C in the RTL description. The two paths include one extending from A_reg to C_reg through OR—1 and AND—1, and the other extending from A_reg to C_reg through INV—1, OR—2 and AND—1. The following malfunction may be caused in such an asynchronous circuit.
FIG. 3 illustrates an example of the malfunction caused in the asynchronous circuit.
More specifically, FIG. 3 illustrates the simulation result of the asynchronous circuit in FIG. 2B. Note that an output signal of B_reg, i.e., B_reg.Q, is assumed to be 0 and is omitted from FIG. 3. Various signals in FIG. 3 represent corresponding signals indicated in FIG. 2B.
According to the RTL description in FIG. 2A, when B=0 and C=0 are held, a value of C does not become 1 even if a value of A takes 1. In the asynchronous circuit illustrated in FIG. 2B, however, there may cause a hazard that an input of C_reg, i.e., C_reg.DATA, becomes 1 for a short period due to a delay difference in the combined circuit. If the clock signal CK1 rises in such a period (malfunction generating period), C_reg.Q becomes 1 and a malfunction occurs. For that reason, verification of the asynchronous circuit has to be performed after the netlist has been produced.
In order to find the above-described malfunction, however, the simulation is required to be executed while changing the phase of the clock signal CK1 little by little so that the clock signal CK1 rises during the malfunction generating period. This leads to the problem that the simulation takes a very long time and has a difficulty in finding a malfunction. At present, therefore, when a malfunction is found in the stage of operation confirmation based on evaluation of the actual chip, verification is executed by measuring a phase difference of the asynchronous clocks and reproducing the malfunction through simulation based on the netlist. That verification takes a very long time and has a high cost.